The present invention relates to the field of computer systems, and more specifically to a method and system for formal verification of a circuit model.
One method of verifying a circuit design is called formal verification. Formal verification is the use of mathematical techniques to formally (i.e. without simulating circuit input vectors) compare circuit design models which are at different levels of abstraction to establish logic functionality equivalence between the two models. For example, formal verification is used to compare the specification of a logic circuit in some hardware description language (HDL) against its implementation as a schematic model.
Formal verification tools are often based on binary decision diagrams (BDDs). BDDs are directed acyclic graph structures that encode the value of a boolean logic function for all possible input value combinations. BDDs simplify the task of boolean function equivalence, since BDDs have efficient algorithms for equivalence checking and other boolean operations.
However, BDD techniques suffer from exponential memory requirements since the size of the BDD representing a given circuit can grow exponentially relative to the inputs of the circuit. To overcome this, solutions based on a divide-and-conquer approach have been developed. These techniques attempt to partition the specification and implementation circuit models along frontiers of equivalent signal pairs called cut-points. The resulting sub-circuit partitions of each circuit model are independently analyzed, thus breaking the verification task into manageable units.
However, one problem that arises when introducing cut-points into circuit models is that the verification method may return a false negative. False negatives appear when the technique that compares the two circuits classifies them as different, while in reality they are not. Thus, cut-point based formal verification techniques include a process of eliminating false negatives by attempting to determine whether the corresponding circuit outputs are truly different or the algorithm produced a false negative. This extra step is time-consuming.
Accordingly, for the reasons stated above, and for other reasons stated below which will be appreciated by those skilled in the art upon reading and understanding the present specification, there is a need in the art for a method of verifying circuit models which is faster and permits the verification of more complex circuits within a formal mathematical framework.